#ifndef A_FEATURETERM
#define A_FEATURETERM

#include "assert.h"

class UnificationBinding {
public:
	UnificationBinding(FeatureTerm *f1,FeatureTerm *f2,FeatureTerm *u) {
		if (f1!=0) m_f1=new FeatureTerm(f1);
			  else m_f1=0;
		if (f2!=0) m_f2=new FeatureTerm(f2);
			  else m_f2=0;
		m_u=new FeatureTerm(u);
	};
	UnificationBinding(UnificationBinding &b) {
		if (b.m_f1!=0) m_f1=new FeatureTerm(b.m_f1);
				  else m_f1=0;
		if (b.m_f2!=0) m_f2=new FeatureTerm(b.m_f2);
				  else m_f2=0;
		if (b.m_u!=0) m_u=new FeatureTerm(b.m_u);
				 else m_u=0;
	};

	~UnificationBinding() {
		if (m_f1!=0) delete m_f1;
		m_f1=0;
		if (m_f2!=0) delete m_f2;
		m_f2=0;
		if (m_u!=0) delete m_u;
		m_u=0;
	}

	FeatureTerm *m_f1,*m_f2,*m_u;
};


class UnificationResult {
public:
	UnificationResult() {
		m_u=0;
	};

	UnificationResult(UnificationResult &r) {
		if (r.m_u!=0) m_u=new FeatureTerm(r.m_u);
				 else m_u=0;

		m_bindings.Copy(r.m_bindings);	
		m_stack.Copy(r.m_stack);
	};

	UnificationResult *clone(FTKBase *dm) {
		UnificationResult *r=new UnificationResult();
		UnificationBinding *b;
		List<FeatureTerm> l,*l2;
		FeatureTerm *u;

		if (m_u!=0) l.Add(m_u);

		m_bindings.Rewind();
		while(m_bindings.Iterate(b)) {
			l.Add(b->m_u);
		} // while

		m_stack.Rewind();
		while(m_stack.Iterate(u)) l.Add(u);

		l2=FeatureTerm::clone(&l,dm);

		l.ExtractAll();

		if (m_u!=0) r->m_u=l2->ExtractIni();

		m_bindings.Rewind();
		while(m_bindings.Iterate(b)) {
			u=l2->ExtractIni();
			assert(b->m_u->getDataType()==u->getDataType());
			r->m_bindings.Add(new UnificationBinding(b->m_f1,b->m_f2,u));
			delete u;
		} // while

		while(!l2->EmptyP()) r->m_stack.Add(l2->ExtractIni());

		delete l2;
		return r;
	};


	void substitute(FeatureTerm *f1,FeatureTerm *f2) {
		FeatureTerm *u;
		UnificationBinding *b;

		if (m_u!=0) m_u->substitute(f1,f2);
		m_bindings.Rewind();
		while(m_bindings.Iterate(b)) b->m_u->substitute(f1,f2);
		m_stack.Rewind();
		while(m_stack.Iterate(u)) u->substitute(f1,f2);
	};


	~UnificationResult() {
		delete m_u;
	};

	FeatureTerm *m_u;
	List<UnificationBinding> m_bindings;
	List<FeatureTerm> m_stack;
};




FeatureTerm *simple_unification(FeatureTerm *f1,FeatureTerm *f2,Ontology *ontology,FTKBase *domain_model);

List<FeatureTerm> *unification(FeatureTerm *f1,FeatureTerm *f2,Ontology *ontology,FTKBase *domain_model);
List<UnificationResult> *unification_with_bindings(FeatureTerm *f1,FeatureTerm *f2,Ontology *ontology,FTKBase *domain_model);

List<UnificationResult> *ft_internal_unification(FeatureTerm *f1,FeatureTerm *f2,List<UnificationBinding> *bindings,List<FeatureTerm> *stack,Ontology *ontology,FTKBase *domain_model);
List<UnificationResult> *set_internal_unification(FeatureTerm *f1,FeatureTerm *f2,List<UnificationBinding> *bindings,List<FeatureTerm> *stack,Ontology *ontology,FTKBase *domain_model,bool singleton);

FeatureTerm *integer_unification(FeatureTerm *f1,FeatureTerm *f2,FeatureTerm *U,Ontology *o);
FeatureTerm *float_unification(FeatureTerm *f1,FeatureTerm *f2,FeatureTerm *U,Ontology *o);


#endif
